<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>100 theorems in Lean</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

  <div class="row mt-3">
    <div class="col">
        <h1>100 theorems</h1>

        <p><a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk</a> maintains <a href="https://www.cs.ru.nl/~freek/100/">a list</a> tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers.
        Currently 44 of them are formalized in Lean:</p>

  <div class="list-group">
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="1">1: The Irrationality of the Square Root of 2 <a class="hover-link" href="#1">#</a></h5>
        <h6 class="card-title">Author: mathlib</h6>
        
        
        <span class="doc-stmt nm">irrational_sqrt_two</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">irrational (real.sqrt 2)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/real/irrational.html#irrational_sqrt_two">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/real/irrational.lean#L84">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="2">2: Fundamental Theorem of Algebra <a class="hover-link" href="#2">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">complex.exists_root</span>
         <span class="doc-stmt arg">{f : polynomial ℂ}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">0 < f.degree →
(∃ (z : ℂ), f.is_root z)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/complex/polynomial.html#complex.exists_root">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/complex/polynomial.lean#L34">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="3">3: The Denumerability of the Rational Numbers <a class="hover-link" href="#3">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">rat.denumerable</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">denumerable ℚ</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/rat/denumerable.html#rat.denumerable">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/rat/denumerable.lean#L21">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="4">4: Pythagorean Theorem <a class="hover-link" href="#4">#</a></h5>
        <h6 class="card-title">Author: Joseph Myers</h6>
        
        
        <span class="doc-stmt nm">euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two</span>
         <span class="doc-stmt arg">(V : Type u_1)</span> <span class="doc-stmt arg">{P : Type u_2}</span> <span class="doc-stmt arg">[inner_product_space V]</span> <span class="doc-stmt arg">[metric_space P]</span> <span class="doc-stmt arg">[euclidean_affine_space V P]</span> <span class="doc-stmt arg">(p1 p2 p3 : P)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">has_dist.dist p1 p3 * has_dist.dist p1 p3 =
    has_dist.dist p1 p2 *
        has_dist.dist p1 p2 +
      has_dist.dist p3 p2 *
        has_dist.dist p3 p2 ↔
  euclidean_geometry.angle V p1 p2 p3 =
    real.pi / 2</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/geometry/euclidean.html#euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/geometry/euclidean.lean#L591">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="7">7: Law of Quadratic Reciprocity <a class="hover-link" href="#7">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">zmod.quadratic_reciprocity</span>
         <span class="doc-stmt arg">(p q : ℕ)</span> <span class="doc-stmt arg">[fact (nat.prime p)]</span> <span class="doc-stmt arg">[fact (nat.prime q)]</span> <span class="doc-stmt arg">[hp1 : fact (p % 2 = 1)]</span> <span class="doc-stmt arg">[hq1 : fact (q % 2 = 1)]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">p ≠ q →
zmod.legendre_sym p q *
    zmod.legendre_sym q p =
  (-1) ^ (p / 2 * (q / 2))</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/number_theory/quadratic_reciprocity.html#zmod.quadratic_reciprocity">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/number_theory/quadratic_reciprocity.lean#L443">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="10">10: Euler’s Generalization of Fermat’s Little Theorem <a class="hover-link" href="#10">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">nat.modeq.pow_totient</span>
         <span class="doc-stmt arg">{x n : ℕ}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">x.coprime n →
x ^ n.totient ≡
  1 [MOD
  n]</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/field_theory/finite.html#nat.modeq.pow_totient">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/field_theory/finite.lean#L251">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="11">11: The Infinitude of Primes <a class="hover-link" href="#11">#</a></h5>
        <h6 class="card-title">Author: Jeremy Avigad</h6>
        
        
        <span class="doc-stmt nm">nat.exists_infinite_primes</span>
         <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">∃ (p : ℕ), n ≤ p ∧ nat.prime p</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/nat/prime.html#nat.exists_infinite_primes">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/nat/prime.lean#L322">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="17">17: De Moivre’s Theorem <a class="hover-link" href="#17">#</a></h5>
        <h6 class="card-title">Author: Abhimanyu Pallavi Sudhir</h6>
        
        
        <span class="doc-stmt nm">complex.cos_add_sin_mul_I_pow</span>
         <span class="doc-stmt arg">(n : ℕ)</span> <span class="doc-stmt arg">(z : ℂ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(complex.cos z +
       complex.sin z * complex.I) ^
    n =
  complex.cos (↑n * z) +
    complex.sin (↑n * z) *
      complex.I</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/complex/exponential.html#complex.cos_add_sin_mul_I_pow">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/complex/exponential.lean#L745">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="19">19: Four Squares Theorem <a class="hover-link" href="#19">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">nat.sum_four_squares</span>
         <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">∃ (a b c d : ℕ),
  a ^ 2 + b ^ 2 +
        c ^ 2 +
      d ^ 2 =
    n</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/number_theory/sum_four_squares.html#nat.sum_four_squares">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/number_theory/sum_four_squares.lean#L195">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="20">20: All Primes (1 mod 4) Equal the Sum of Two Squares <a class="hover-link" href="#20">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">nat.prime.sum_two_squares</span>
         <span class="doc-stmt arg">(p : ℕ)</span> <span class="doc-stmt arg">[hp : fact (nat.prime p)]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">p % 4 = 1 →
(∃ (a b : ℕ), a ^ 2 + b ^ 2 = p)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/number_theory/sum_two_squares.html#nat.prime.sum_two_squares">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/number_theory/sum_two_squares.lean#L21">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="22">22: The Non-Denumerability of the Continuum <a class="hover-link" href="#22">#</a></h5>
        <h6 class="card-title">Author: Floris van Doorn</h6>
        
        
        <span class="doc-stmt nm">cardinal.not_countable_real</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">¬set.univ.countable</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/real/cardinality.html#cardinal.not_countable_real">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/real/cardinality.lean#L121">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="24">24: The Undecidability of the Continuum Hypothesis <a class="hover-link" href="#24">#</a></h5>
        <h6 class="card-title">Author: Jesse Michael Han and Floris van Doorn</h6>
        
        
        <p><a href="https://github.com/flypitch/flypitch/blob/master/src/summary.lean">result</a></p><p><a href="https://flypitch.github.io/">website</a></p>
        <p><p>see the <code>README</code> file in the <a href="https://github.com/flypitch/flypitch/">linked repository</a>.</p></p>
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="25">25: Schroeder-Bernstein Theorem <a class="hover-link" href="#25">#</a></h5>
        <h6 class="card-title">Author: Mario Carneiro</h6>
        
        
        <span class="doc-stmt nm">function.embedding.schroeder_bernstein</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">{β : Type v}</span> <span class="doc-stmt arg">{f : α → β}</span> <span class="doc-stmt arg">{g : β → α}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">function.injective f →
function.injective g →
(∃ (h : α → β), function.bijective h)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/set_theory/schroeder_bernstein.html#function.embedding.schroeder_bernstein">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/set_theory/schroeder_bernstein.lean#L22">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="27">27: Sum of the Angles of a Triangle <a class="hover-link" href="#27">#</a></h5>
        <h6 class="card-title">Author: Joseph Myers</h6>
        
        
        <span class="doc-stmt nm">euclidean_geometry.angle_add_angle_add_angle_eq_pi</span>
         <span class="doc-stmt arg">(V : Type u_1)</span> <span class="doc-stmt arg">{P : Type u_2}</span> <span class="doc-stmt arg">[inner_product_space V]</span> <span class="doc-stmt arg">[metric_space P]</span> <span class="doc-stmt arg">[euclidean_affine_space V P]</span> <span class="doc-stmt arg">{p1 p2 p3 : P}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">p2 ≠ p1 →
p3 ≠ p1 →
euclidean_geometry.angle V p1 p2 p3 +
      euclidean_geometry.angle V p2 p3 p1 +
    euclidean_geometry.angle V p3 p1 p2 =
  real.pi</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/geometry/euclidean.html#euclidean_geometry.angle_add_angle_add_angle_eq_pi">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/geometry/euclidean.lean#L638">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="31">31: Ramsey’s Theorem <a class="hover-link" href="#31">#</a></h5>
        <h6 class="card-title">Author: Bhavik Mehta</h6>
        
        
        <p><a href="https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean">result</a></p>
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="34">34: Divergence of the Harmonic Series <a class="hover-link" href="#34">#</a></h5>
        <h6 class="card-title">Author: Anatole Dedecker</h6>
        
        
        <span class="doc-stmt nm">harmonic_tendsto_at_top</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">filter.tendsto harmonic_series filter.at_top
  filter.at_top</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/specific_limits.html#harmonic_tendsto_at_top">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/specific_limits.lean#L712">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="38">38: Arithmetic Mean/Geometric Mean <a class="hover-link" href="#38">#</a></h5>
        <h6 class="card-title">Author: Yury G. Kudryashov</h6>
        
        
        <span class="doc-stmt nm">real.geom_mean_le_arith_mean_weighted</span>
         <span class="doc-stmt arg">{ι : Type u}</span> <span class="doc-stmt arg">(s : finset ι)</span> <span class="doc-stmt arg">(w z : ι → ℝ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(∀ (i : ι), i ∈ s → 0 ≤ w i) →
s.sum (λ (i : ι), w i) = 1 →
(∀ (i : ι), i ∈ s → 0 ≤ z i) →
s.prod (λ (i : ι), z i ^ w i) ≤
  s.sum (λ (i : ι), w i * z i)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/mean_inequalities.html#real.geom_mean_le_arith_mean_weighted">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/mean_inequalities.lean#L118">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="39">39: Solutions to Pell’s Equation <a class="hover-link" href="#39">#</a></h5>
        <h6 class="card-title">Author: Mario Carneiro</h6>
        
        
        <span class="doc-stmt nm">pell.eq_pell</span>
         <span class="doc-stmt arg">{a : ℕ}</span> <span class="doc-stmt arg">(a1 : 1 < a)</span> <span class="doc-stmt arg">{x y : ℕ}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">x * x -
    d a1 * y * y =
  1 →
(∃ (n : ℕ),
   x = pell.xn a1 n ∧ y = pell.yn a1 n)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/number_theory/pell.html#pell.eq_pell">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/number_theory/pell.lean#L165">source</a></p>
        
        
        <p><p><code>d</code> is defined to be <code>a*a - 1</code> for an arbitrary <code>a &gt; 1</code>.</p></p>
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="42">42: Sum of the Reciprocals of the Triangular Numbers <a class="hover-link" href="#42">#</a></h5>
        <h6 class="card-title">Author: Jalex Stark, Yury Kudryashov</h6>
        
        
        <p><a href="https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/42_inverse_triangle_sum.lean">mathlib archive</a></p>
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="44">44: The Binomial Theorem <a class="hover-link" href="#44">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">add_pow</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">[comm_semiring α]</span> <span class="doc-stmt arg">(x y : α)</span> <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(x + y) ^ n =
  (finset.range (n + 1)).sum
    (λ (m : ℕ),
       x ^ m *
           y ^ (n - m) *
         ↑(n.choose m))</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/nat/choose.html#add_pow">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/nat/choose.lean#L115">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="51">51: Wilson’s Theorem <a class="hover-link" href="#51">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">zmod.wilsons_lemma</span>
         <span class="doc-stmt arg">(p : ℕ)</span> <span class="doc-stmt arg">[fact (nat.prime p)]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">↑((p - 1).fact) = -1</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/number_theory/quadratic_reciprocity.html#zmod.wilsons_lemma">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/number_theory/quadratic_reciprocity.lean#L118">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="52">52: The Number of Subsets of a Set <a class="hover-link" href="#52">#</a></h5>
        <h6 class="card-title">Author: mathlib</h6>
        
        
        <span class="doc-stmt nm">finset.card_powerset</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">(s : finset α)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">s.powerset.card =
  2 ^ s.card</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/finset/powerset.html#finset.card_powerset">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/finset/powerset.lean#L43">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="58">58: Formula for the Number of Combinations <a class="hover-link" href="#58">#</a></h5>
        <h6 class="card-title">Author: mathlib <!--Jeremy Avigad in lean 2--></h6>
        
        
        <span class="doc-stmt nm">finset.card_powerset_len</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">(n : ℕ)</span> <span class="doc-stmt arg">(s : finset α)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(finset.powerset_len n s).card =
  s.card.choose n</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/finset/powerset.html#finset.card_powerset_len">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/finset/powerset.lean#L91">source</a></p>
        
        <span class="doc-stmt nm">finset.mem_powerset_len</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">{n : ℕ}</span> <span class="doc-stmt arg">{s t : finset α}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">s ∈ finset.powerset_len n t ↔
  s ⊆ t ∧ s.card = n</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/finset/powerset.html#finset.mem_powerset_len">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/finset/powerset.lean#L82">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="60">60: Bezout’s Theorem <a class="hover-link" href="#60">#</a></h5>
        <h6 class="card-title">Author: mathlib</h6>
        
        
        <span class="doc-stmt nm">nat.gcd_eq_gcd_ab</span>
         <span class="doc-stmt arg">(x y : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">↑(x.gcd y) =
  ↑x * x.gcd_a y +
    ↑y * x.gcd_b y</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/int/gcd.html#nat.gcd_eq_gcd_ab">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/int/gcd.lean#L77">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="63">63: Cantor’s Theorem <a class="hover-link" href="#63">#</a></h5>
        <h6 class="card-title">Author: mathlib <!-- Mario and/or Johannes --></h6>
        
        
        <span class="doc-stmt nm">cardinal.cantor</span>
         <span class="doc-stmt arg">(a : cardinal)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">a < 2 ^ a</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/set_theory/cardinal.html#cardinal.cantor">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/set_theory/cardinal.lean#L309">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="65">65: Isosceles Triangle Theorem <a class="hover-link" href="#65">#</a></h5>
        <h6 class="card-title">Author: Joseph Myers</h6>
        
        
        <span class="doc-stmt nm">euclidean_geometry.angle_eq_angle_of_dist_eq</span>
         <span class="doc-stmt arg">(V : Type u_1)</span> <span class="doc-stmt arg">{P : Type u_2}</span> <span class="doc-stmt arg">[inner_product_space V]</span> <span class="doc-stmt arg">[metric_space P]</span> <span class="doc-stmt arg">[euclidean_affine_space V P]</span> <span class="doc-stmt arg">{p1 p2 p3 : P}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">has_dist.dist p1 p2 = has_dist.dist p1 p3 →
euclidean_geometry.angle V p1 p2 p3 =
  euclidean_geometry.angle V p1 p3 p2</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/geometry/euclidean.html#euclidean_geometry.angle_eq_angle_of_dist_eq">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/geometry/euclidean.lean#L615">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="66">66: Sum of a Geometric Series <a class="hover-link" href="#66">#</a></h5>
        <h6 class="card-title">Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)</h6>
        
        
        <span class="doc-stmt nm">geom_sum</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[division_ring α]</span> <span class="doc-stmt arg">{x : α}</span> <span class="doc-stmt arg">(h : x ≠ 1)</span> <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">geom_series x n =
  (x ^ n - 1) / (x - 1)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/geom_sum.html#geom_sum">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/geom_sum.lean#L150">source</a></p>
        
        <span class="doc-stmt nm">nnreal.has_sum_geometric</span>
         <span class="doc-stmt arg">{r : nnreal}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">r < 1 →
has_sum (λ (n : ℕ), r ^ n)
  (1 - r)⁻¹</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/specific_limits.html#nnreal.has_sum_geometric">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/specific_limits.lean#L297">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="68">68: Sum of an arithmetic series <a class="hover-link" href="#68">#</a></h5>
        <h6 class="card-title">Author: Johannes Hölzl</h6>
        
        
        <span class="doc-stmt nm">finset.sum_range_id</span>
         <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(finset.range n).sum (λ (i : ℕ), i) =
  n * (n - 1) / 2</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/intervals.html#finset.sum_range_id">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/big_operators/intervals.lean#L134">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="69">69: Greatest Common Divisor Algorithm <a class="hover-link" href="#69">#</a></h5>
        <h6 class="card-title">Author: mathlib</h6>
        
        
        <span class="doc-stmt nm">euclidean_domain.gcd</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[euclidean_domain α]</span> <span class="doc-stmt arg">[decidable_eq α]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">α → α → α</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#euclidean_domain.gcd">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/euclidean_domain.lean#L151">source</a></p>
        
        <span class="doc-stmt nm">euclidean_domain.gcd_dvd</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[euclidean_domain α]</span> <span class="doc-stmt arg">[decidable_eq α]</span> <span class="doc-stmt arg">(a b : α)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">euclidean_domain.gcd a b ∣ a ∧
  euclidean_domain.gcd a b ∣ b</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#euclidean_domain.gcd_dvd">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/euclidean_domain.lean#L167">source</a></p>
        
        <span class="doc-stmt nm">euclidean_domain.dvd_gcd</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[euclidean_domain α]</span> <span class="doc-stmt arg">[decidable_eq α]</span> <span class="doc-stmt arg">{a b c : α}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">c ∣ a →
c ∣ b → c ∣ euclidean_domain.gcd a b</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#euclidean_domain.dvd_gcd">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/euclidean_domain.lean#L182">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="71">71: Order of a Subgroup <a class="hover-link" href="#71">#</a></h5>
        <h6 class="card-title">Author: mathlib</h6>
        
        
        <span class="doc-stmt nm">card_subgroup_dvd_card</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">[group α]</span> <span class="doc-stmt arg">[fintype α]</span> <span class="doc-stmt arg">(s : subgroup α)</span> <span class="doc-stmt arg">[fintype ↥s]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">fintype.card ↥s ∣ fintype.card α</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/group_theory/order_of_element.html#card_subgroup_dvd_card">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/group_theory/order_of_element.lean#L71">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="72">72: Sylow’s Theorem <a class="hover-link" href="#72">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">sylow.exists_subgroup_card_pow_prime</span>
         <span class="doc-stmt arg">{G : Type u}</span> <span class="doc-stmt arg">[group G]</span> <span class="doc-stmt arg">[fintype G]</span> <span class="doc-stmt arg">(p : ℕ)</span> <span class="doc-stmt arg">{n : ℕ}</span> <span class="doc-stmt arg">[hp : fact (nat.prime p)]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">p ^ n ∣ fintype.card G →
(∃ (H : subgroup G),
   fintype.card ↥H = p ^ n)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/group_theory/sylow.html#sylow.exists_subgroup_card_pow_prime">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/group_theory/sylow.lean#L197">source</a></p>
        
        <p><a href="https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L885">sylow_conjugate</a></p><p><a href="https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L925">card_sylow_dvd</a></p><p><a href="https://github.com/ChrisHughes24/Sylow/blob/7185e33eeb6d28ea1a423492e7b4a8634aa9723d/src/sylow.lean#L944">card_sylow_modeq_one</a></p>
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="73">73: Ascending or Descending Sequences <a class="hover-link" href="#73">#</a></h5>
        <h6 class="card-title">Author: Bhavik Mehta</h6>
        
        
        <p><a href="https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/73_ascending_descending_sequences.lean">mathlib archive</a></p>
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="74">74: The Principle of Mathematical Induction <a class="hover-link" href="#74">#</a></h5>
        <h6 class="card-title">Author: Leonardo de Moura</h6>
        
        
        <span class="doc-stmt nm">nat</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">Type</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/core/init/core.html#nat">docs</a>, <a href="https://github.com/leanprover-community/lean/blob/f539be1/library/init/core.lean#L305">source</a></p>
        
        
        <p><p>Automatically generated when defining the natural numbers</p></p>
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="75">75: The Mean Value Theorem <a class="hover-link" href="#75">#</a></h5>
        <h6 class="card-title">Author: Yury G. Kudryashov</h6>
        
        
        <span class="doc-stmt nm">exists_deriv_eq_slope</span>
         <span class="doc-stmt arg">(f : ℝ → ℝ)</span> <span class="doc-stmt arg">{a b : ℝ}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">a < b →
continuous_on f (set.Icc a b) →
differentiable_on ℝ f (set.Ioo a b) →
(∃ (c : ℝ) (H : c ∈ set.Ioo a b),
   deriv f c =
     (f b - f a) / (b - a))</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/calculus/mean_value.html#exists_deriv_eq_slope">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/calculus/mean_value.lean#L599">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="78">78: The Cauchy-Schwarz Inequality <a class="hover-link" href="#78">#</a></h5>
        <h6 class="card-title">Author: Zhouhang Zhou</h6>
        
        
        <span class="doc-stmt nm">inner_mul_inner_self_le</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[inner_product_space α]</span> <span class="doc-stmt arg">(x y : α)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">has_inner.inner x y *
    has_inner.inner x y ≤
  has_inner.inner x x * has_inner.inner y y</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_mul_inner_self_le">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/normed_space/real_inner_product.lean#L339">source</a></p>
        
        <span class="doc-stmt nm">abs_inner_le_norm</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">[inner_product_space α]</span> <span class="doc-stmt arg">(x y : α)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">abs (has_inner.inner x y) ≤
  ∥x∥ *
    ∥y∥</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#abs_inner_le_norm">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/normed_space/real_inner_product.lean#L377">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="79">79: The Intermediate Value Theorem <a class="hover-link" href="#79">#</a></h5>
        <h6 class="card-title">Author: mathlib (Rob Lewis and Chris Hughes)</h6>
        
        
        <span class="doc-stmt nm">intermediate_value_Icc</span>
         <span class="doc-stmt arg">{α : Type u}</span> <span class="doc-stmt arg">{β : Type v}</span> <span class="doc-stmt arg">[conditionally_complete_linear_order α]</span> <span class="doc-stmt arg">[topological_space α]</span> <span class="doc-stmt arg">[order_topology α]</span> <span class="doc-stmt arg">[conditionally_complete_linear_order β]</span> <span class="doc-stmt arg">[topological_space β]</span> <span class="doc-stmt arg">[order_topology β]</span> <span class="doc-stmt arg">[densely_ordered α]</span> <span class="doc-stmt arg">{a b : α}</span> <span class="doc-stmt arg">(hab : a ≤ b)</span> <span class="doc-stmt arg">{f : α → β}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">continuous_on f (set.Icc a b) →
set.Icc (f a) (f b) ⊆ f '' set.Icc a b</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#intermediate_value_Icc">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/topology/algebra/ordered.lean#L1860">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="80">80: The Fundamental Theorem of Arithmetic <a class="hover-link" href="#80">#</a></h5>
        <h6 class="card-title">Author: mathlib (Chris Hughes)</h6>
        
        
        <span class="doc-stmt nm">nat.factors_unique</span>
         <span class="doc-stmt arg">{n : ℕ}</span> <span class="doc-stmt arg">{l : list ℕ}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">l.prod = n →
(∀ (p : ℕ), p ∈ l → nat.prime p) →
l ~ n.factors</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/nat/prime.html#nat.factors_unique">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/nat/prime.lean#L538">source</a></p>
        
        <span class="doc-stmt nm">int.euclidean_domain</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">euclidean_domain ℤ</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/algebra/euclidean_domain.html#int.euclidean_domain">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/algebra/euclidean_domain.lean#L332">source</a></p>
        
        <span class="doc-stmt nm">euclidean_domain.to_principal_ideal_domain</span>
         <span class="doc-stmt arg">{R : Type u}</span> <span class="doc-stmt arg">[euclidean_domain R]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">is_principal_ideal_ring R</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/ring_theory/principal_ideal_domain.html#euclidean_domain.to_principal_ideal_domain">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/ring_theory/principal_ideal_domain.lean#L106">source</a></p>
        
        <span class="doc-stmt nm">unique_factorization_domain</span>
         <span class="doc-stmt arg">(α : Type u_2)</span> <span class="doc-stmt arg">[integral_domain α]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">Type u_2</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/ring_theory/unique_factorization_domain.html#unique_factorization_domain">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/ring_theory/unique_factorization_domain.lean#L30">source</a></p>
        
        <span class="doc-stmt nm">unique_factorization_domain.unique</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">[integral_domain α]</span> <span class="doc-stmt arg">[unique_factorization_domain α]</span> <span class="doc-stmt arg">{f g : multiset α}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">(∀ (x : α), x ∈ f → irreducible x) →
(∀ (x : α), x ∈ g → irreducible x) →
associated f.prod g.prod →
multiset.rel associated f g</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/ring_theory/unique_factorization_domain.html#unique_factorization_domain.unique">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/ring_theory/unique_factorization_domain.lean#L91">source</a></p>
        
        
        <p><p>it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.</p></p>
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="82">82: Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) <a class="hover-link" href="#82">#</a></h5>
        <h6 class="card-title">Author: Floris van Doorn</h6>
        
        
        <p><a href="https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/82_cubing_a_cube.lean">mathlib archive</a></p>
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="85">85: Divisibility by 3 Rule <a class="hover-link" href="#85">#</a></h5>
        <h6 class="card-title">Author: Scott Morrison</h6>
        
        
        <span class="doc-stmt nm">three_dvd_iff</span>
         <span class="doc-stmt arg">(n : ℕ)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">3 ∣ n ↔ 3 ∣ (digits 10 n).sum</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/nat/digits.html#three_dvd_iff">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/nat/digits.lean#L527">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="86">86: Lebesgue Measure and Integration <a class="hover-link" href="#86">#</a></h5>
        <h6 class="card-title">Author: Johannes Hölzl</h6>
        
        
        <span class="doc-stmt nm">measure_theory.lintegral</span>
         <span class="doc-stmt arg">{α : Type u_1}</span> <span class="doc-stmt arg">[measurable_space α]</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">measure_theory.measure α →
(α → ennreal) → ennreal</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/measure_theory/integration.html#measure_theory.lintegral">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/measure_theory/integration.lean#L782">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="89">89: The Factor and Remainder Theorems <a class="hover-link" href="#89">#</a></h5>
        <h6 class="card-title">Author: Chris Hughes</h6>
        
        
        <span class="doc-stmt nm">polynomial.dvd_iff_is_root</span>
         <span class="doc-stmt arg">{R : Type u}</span> <span class="doc-stmt arg">{a : R}</span> <span class="doc-stmt arg">[comm_ring R]</span> <span class="doc-stmt arg">{p : polynomial R}</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">polynomial.X -
      ⇑polynomial.C a ∣
    p ↔
  p.is_root a</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/div.html#polynomial.dvd_iff_is_root">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/polynomial/div.lean#L533">source</a></p>
        
        <span class="doc-stmt nm">polynomial.mod_X_sub_C_eq_C_eval</span>
         <span class="doc-stmt arg">{R : Type u}</span> <span class="doc-stmt arg">[field R]</span> <span class="doc-stmt arg">(p : polynomial R)</span> <span class="doc-stmt arg">(a : R)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">p %
    (polynomial.X -
       ⇑polynomial.C a) =
  ⇑polynomial.C (polynomial.eval a p)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/data/polynomial/field_division.html#polynomial.mod_X_sub_C_eq_C_eval">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/data/polynomial/field_division.lean#L109">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="91">91: The Triangle Inequality <a class="hover-link" href="#91">#</a></h5>
        <h6 class="card-title">Author: Zhouhang Zhou</h6>
        
        
        <span class="doc-stmt nm">inner_product_space.to_normed_group</span>
        
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">normed_group α</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_product_space.to_normed_group">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/analysis/normed_space/real_inner_product.lean#L75">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="94">94: The Law of Cosines <a class="hover-link" href="#94">#</a></h5>
        <h6 class="card-title">Author: Joseph Myers</h6>
        
        
        <span class="doc-stmt nm">euclidean_geometry.dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle</span>
         <span class="doc-stmt arg">(V : Type u_1)</span> <span class="doc-stmt arg">{P : Type u_2}</span> <span class="doc-stmt arg">[inner_product_space V]</span> <span class="doc-stmt arg">[metric_space P]</span> <span class="doc-stmt arg">[euclidean_affine_space V P]</span> <span class="doc-stmt arg">(p1 p2 p3 : P)</span>
        <span class="doc-stmt sep">:</span>
        <div class="doc-stmt tp">has_dist.dist p1 p3 * has_dist.dist p1 p3 =
  has_dist.dist p1 p2 *
        has_dist.dist p1 p2 +
      has_dist.dist p3 p2 *
        has_dist.dist p3 p2 -
    2 * has_dist.dist p1 p2 *
        has_dist.dist p3 p2 *
      real.cos (euclidean_geometry.angle V p1 p2 p3)</div>
        <p><a href="https://leanprover-community.github.io/mathlib_docs/geometry/euclidean.html#euclidean_geometry.dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle">docs</a>, <a href="https://github.com/leanprover-community/mathlib/blob/f8fd0c3/src/geometry/euclidean.lean#L600">source</a></p>
        
        
        
    </div>
    
    <div class="list-group-item">
        <h5 class="card-title markdown-heading" id="96">96: Principle of Inclusion/Exclusion <a class="hover-link" href="#96">#</a></h5>
        <h6 class="card-title">Author: Neil Strickland</h6>
        
        
        <p><a href="https://github.com/NeilStrickland/lean_lib/blob/f88d162da2f990b87c4d34f5f46bbca2bbc5948e/src/combinatorics/matching.lean#L304">github</a></p>
        
    </div>
    
  </div>


  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>